Lambda the Ultimate

Bertrand Meyer yet again has lined up a fantastic set of speakers for this year's LASER summerschool that targets some very relevant and timely topics in our field:

• Tryggve Fossum, Intel Fellow and Director of Microarchitecture Development, Intel Corporation on Chip level Multi Processors
• Maurice Herlihy, Brown University on The Art of Multiprocessor Programming
• Bertrand Meyer, ETH Zurich and Eiffel Software on Correct Contract-Covered Concurrent Computation
• Robin Milner, Cambridge University on Bigraphs: a space for mobile interaction
• Peter O'Hearn, Queen Mary University of London on Proof Techniques for Concurrent Programs
• Daniel A. Reed, Microsoft Research and UNC Chapel Hill on Living in the Multicore Computing Clouds

Coding Horror is a popular programming blog. A recent post concerns type inference in C#:

C# ... offers implicitly typed local variables. ... It's not dynamic typing, per se; C# is still very much a statically typed language. It's more of a compiler trick, a baby step toward a world of Static Typing Where Possible, and Dynamic Typing When Needed.

... I use implicit variable typing whenever and wherever it makes my code more concise. Anything that removes redundancy from our code should be aggressively pursued -- up to and including switching languages.

You might even say implicit variable typing is a gateway drug to more dynamically typed languages. And that's a good thing.

I think this post is interesting for a number of reasons, and the link to LtU is just the start. Now it appears the author is confused as to what “implicitly typed local variables” are, confusing local type inference (which they are) with dynamic typing (which they are not). Many commenters also suffer from this confusion. Other commenters rightly note that the inferred type is not always the type the programmers wants (particularly important in the presence of sub-typing). Furthermore, type inference harms readability. I'm reminded of recent discussion on the PLT Scheme mailing list on the merits of local and global type inference. The consensus there seems to be that while local type inference is useful, global inference is not.

So, wise people, what is the future of type inference? How useful is it really, especially when we look at type systems that go beyond what H-M can handle? How are we going to get working programmers to use it, and understand it? Do we need better tool support? Do we have any hope of better education for the average programmer?

By now there is an extensive network of interlocking analogies between physics, topology, logic and computer science, which can be seen most easily by comparing the roles that symmetric monoidal closed categories play in each subject. However, symmetric monoidal categories are just the n = 1, k = 3 entry of a hypothesized “periodic table” of k-tuply monoidal n-categories. This raises the question of how these analogies extend. We present some thoughts on this question, focusing on how monoidal closed 2-categories might let us understand the lambda calculus more deeply.

Link to the talk

via The n-Category Café

Two intensively studied intermediate representations in compiler theory are Static Single Assignment form (SSA) and CPS translations, and Richard Kelsey's 1995 paper, A Correspondence Between Continuation Passing Style and Static Single Assignment Form (.ps.gz) shows a nearly complete, exact equivalence between the two IRs.

The correspondence shows how the imperatively expressed SSA can be regarded as side-effect free, and Andrew Appel has pushed this idea to claim that SSA is functional programming. This result is of clear relevance to discussions turning on "what is purity?", such as here.

As an aside, the Wikipedia article Static Single Assignment form is rather good.

It is generally known that JavaScript supports a functional style of programming. But because it does not have algebraic data types, the functional programming is usually limited to some simple higher order functions applied to Arrays.

I have often build small libraries that allow working with some aspects of algebraic data types in JavaScript. This time I thought is was cool enough to write a bit about it:

Algebraic Data Types in JavaScript

It includes:

• a very small footprint
• unfold, map and fold over any adt
• merging (read deforestation/fusion) of unfold, map and fold
• user defined derived properties (think derived classes Show, Eq...)

I also show how to do the Data Types à la carte style of Wouter Swierstra with this library.

Parametric Higher-Order Abstract Syntax for Mechanized Semantics

We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and translation from a language with ML-style pattern matching to a simpler language with no variable-arity binding constructs. By avoiding the syntactic hassle associated with first-order representation techniques, we achieve a very high degree of proof automation.

I was aware of this some months ago now, but held back commenting on it at Adam's request until it had been accepted for publication, which it now apparently has. This is (one element of) Adam's continued work on LambdaTamer, his Coq-based environment for building certified compilers. There is a new version of LambdaTamer using this parametric higher-order abstract syntax approach. The new version also works in current and future versions of Coq, unlike the previous version. Finally, Adam is apparently working on a paper regarding "type-theoretic denotational semantics for higher order, impure object languages" and is post-docing with Greg Morrisett. The relationship between Adam's work and the YNot project is a bit unclear to me; perhaps either Adam or Greg could help clarify that.

Update: Whoops. I got ahead of myself and neglected to notice that the paper is not actually yet available, although the new version of LambdaTamer is. So at the moment, this story is merely to note that the paper exists and to provide a link to the new LambdaTamer. My apologies to Adam and the LtU readership.

2nd Update: The paper is now available at the link, in either PostScript or PDF form.

Ehud recently lamented the lack of small interpreters for people to play with. I thought I would take this as an invitation share my JavaScript version of Cat that supports turtle graphics:

http://cat-language.com/interpreter.html

The parsing code will definitely make the angels weep and programmers gnash their teeth.

Enjoy!

I just noticed Stroustrup is about to publish this introductory book.

I am stunned on many levels, so I will keep my comments short.

In general, this seems like HTDP for C++, that is it is not a comprehensive text about C++ or about CS in general, but rather one aimed at teaching the basics of software construction. This is a good idea, and many have written books with similar goals in the past, of course.

I wonder what are the chances that any university not employing Stroustrup will switch to C++ for their introductory course (if they are not using it already). It seems to me everyone is teaching Java...

My second observation is that a large fraction of the book is devoted to STL. Which a good thing on many levels. Some of the topics may even be explained functionally.

My third observation is that even given the intended audience and goals the ToC seems really sparse. I wonder if that's all the book is going to contain.

The ACM Curriculum board has re-opened the 2001 design for review. Although ACM is a US-based organization, the curriculum is not only influential at the middle tier of US colleges and universities, but it is also taken seriously by many evolving and developing educational institutions overseas. In recent years, the study of non-OO PLs, and of other key PL topics such as type systems, has grown increasingly marginal in the undergraduate CS curriculum. In particular, the study of functional programming is not included in the ACM CS2001 core. We may now have an opening to make a small change in this situation.

The ACM Curriculum board has agreed to consider a proposal on including FP as an equal to OOP (10 "hours" each) in the standard curriculum. This was the most concrete outcome of the PLC workshop at Harvard two weeks ago. The proposal was drafted by Stuart Reges, Shriram Krishnamurthi, and Matthias Felleisen and was endorsed unanimously by the workshop attendees and by the SIGPLAN Executive Committee. It proceeds on the premise that inclusion of FP in the core curriculum is the most important single thing that the PL community can do for CS education. In particular, this will help prepare students for a properly designed though possibly optional PL course or courses.

Please consider contributing comments to the web site. A simple "Yes, I think this is a great idea" will be helpful. A short explanation is even better.

There is now a long list of comments supporting this proposal. However, we have very few comments from people in industry, so comments from the many non-academics on LtU would be particularly helpful. Examples of how FP has helped you would, I think, be particularly persuasive.

The web site is http://wiki.acm.org/cs2001/index.php?title=SIGPLAN_Proposal. Unfortunately, you must be an ACM member to view or submit comments.

[Edit: This is important enough that I am promoting this item to the front page even though the link is only accessible with an ACM account. The issue itself can be debated in the comments, and hopefully at some point an open mirror of the ACM discussion will be created. -- Ehud]

TileStack is an attempt to resurrect HyperCard and bring it to the web.

Running online there are going to be limitations about which stacks can be ported, which may reduce the usefulness and impact of this project, but maybe a standalone version will come later.

The system compiles Speak (the TileStack version of HyperTalk) to Javascript. If the result is not obfuscated, something I haven't verified, it may be possible to augment the output from TileStack with additional capabilities not supported or not yet implemented.

From the compatibility angle it is interesting to note that they renamed the language and seem to imply they are going to extend it beyond HyperTalk, without giving any specific guarantee about future compatibility. I'd suggest releasing the compiler that's as close to full HyperTalk compatibility as a separate product (or even, if they can bring themselves to do it, releasing it as open source).